poss:(ES{i}Prop{i'}), R:(possible-event{i:l}(poss)possible-event{i:l}(poss)Prop{i'}), P,
Q:(possible-event{i:l}(poss)Prop{i'}).
(e:possible-event{i:l}(poss). P(e)  Q(e))
 (e:possible-event{i:l}
 (e:possible-event(poss).
 (es-knows{i:l}(poss; R; P; e)  es-knows{i:l}(poss; R; Q; e)) 

latex

Definitions	t  T, P  Q, x:A. B(x), x:AB(x), PossibleEvent(poss), f(a), Type, Prop, ES, x:AB(x), K(P)@e
Lemmas	possible-event wf, event system wf